Nuprl Lemma : swap_length 4,23

T:Type, L:T List, ij:||L||. ||swap(L;i;j)|| = ||L||   
latex


Definitionst  T, x:AB(x), ||as||, {i..j}, P  Q, False, A, P & Q, AB, i  j < k, , (ij), swap(L;i;j)
Lemmaspermute list length, flip wf, le wf, int seg wf, length wf1

origin